es:ES, p:(E(E + Top)), a, b, c, d, e:E. c p d  d p e  a p b  b p< c  a p< e 

latex

Definitions	ES, x:AB(x), left + right, Top, E, e p< e', e p e', t  T, x:A. B(x), P  Q
Lemmas	es-p-locl transitivity1, es-p-locl transitivity2, es-p-le wf, es-p-locl wf